# Maintainer: Some One <some.one@some.email.com>

_realname=z3
pkgbase=mingw-w64-${_realname}
pkgname=("${MINGW_PACKAGE_PREFIX}-${_realname}")
pkgver=4.14.1
pkgrel=1
pkgdesc="Z3 is a high-performance theorem prover being developed at Microsoft Research (mingw-w64)"
arch=('any')
mingw_arch=('mingw32' 'mingw64' 'ucrt64' 'clang64' 'clangarm64')
url="https://github.com/Z3Prover/z3"
license=('spdx:MIT')
depends=("${MINGW_PACKAGE_PREFIX}-gcc-libs"
         $([[ ${CARCH} == i686 ]] || echo "${MINGW_PACKAGE_PREFIX}-gmp"))
makedepends=("${MINGW_PACKAGE_PREFIX}-cc"
             "${MINGW_PACKAGE_PREFIX}-cmake"
             "${MINGW_PACKAGE_PREFIX}-ninja"
             "${MINGW_PACKAGE_PREFIX}-python"
             $([[ ${CARCH} == i686 ]] || echo \
               "${MINGW_PACKAGE_PREFIX}-python-build" \
               "${MINGW_PACKAGE_PREFIX}-python-installer" \
               "${MINGW_PACKAGE_PREFIX}-python-setuptools"))
source=("https://github.com/Z3Prover/z3/archive/z3-${pkgver}.tar.gz"
        001-mingw-fixes.patch
        003-fix-dll-exports.patch
        004-fix-python-bindings-install.patch)
sha256sums=('81a02c2c64c64d6c3df233f59186b95627990ada0c4c2fc901c9c25a7072672a'
            'dff9754409a077d0ae49f1bfb2404bd5b318d301273844a80649a9e20e61e2fa'
            'ce01668afae8e60c32a0d7937d3f8f67a7dc23aa4270913d157e676d061dfe6a'
            'a1c96b734e71d4cffc5d55f8a9ed5cc823ac87a8fcb6691a84a23a201398a398')

apply_patch_with_msg() {
  for _fname in "$@"
  do
    msg2 "Applying ${_fname}"
    patch -Nbp1 -i "${srcdir}"/${_fname}
  done
}

prepare() {
  cd "${srcdir}"/${_realname}-${_realname}-${pkgver}
  apply_patch_with_msg \
    001-mingw-fixes.patch \
    003-fix-dll-exports.patch \
    004-fix-python-bindings-install.patch
}

build() {
  local -a extra_config
  if check_option "debug" "y"; then
    extra_config+=(-DCMAKE_BUILD_TYPE=Debug)
    VERBOSE="VERBOSE=1"
  else
    extra_config+=(-DCMAKE_BUILD_TYPE=Release)
  fi

  mkdir -p "${srcdir}"/build-${MSYSTEM}-static && cd "${srcdir}"/build-${MSYSTEM}-static

  msg "Build static z3"
  MSYS2_ARG_CONV_EXCL="-DCMAKE_INSTALL_PREFIX=" \
  ${MINGW_PREFIX}/bin/cmake.exe \
    -G"Ninja" \
    -DCMAKE_INSTALL_PREFIX=${MINGW_PREFIX} \
    -DZ3_BUILD_LIBZ3_SHARED=OFF \
    -DZ3_BUILD_TEST_EXECUTABLES=OFF \
    -DZ3_INCLUDE_GIT_HASH=OFF \
    -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
    -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
    -DPython3_EXECUTABLE=${MINGW_PREFIX}/bin/python.exe \
    "${extra_config[@]}" \
    ../${_realname}-${_realname}-${pkgver}

  ${MINGW_PREFIX}/bin/cmake.exe --build ./

  mkdir -p "${srcdir}"/build-${MSYSTEM}-shared && cd "${srcdir}"/build-${MSYSTEM}-shared

  if [[ ${CARCH} == i686 ]]; then
    extra_config+=("-DZ3_BUILD_PYTHON_BINDINGS=OFF" "-DZ3_USE_LIB_GMP=OFF")
  else
    extra_config+=("-DZ3_BUILD_PYTHON_BINDINGS=ON" "-DZ3_USE_LIB_GMP=ON")
  fi

  msg "Build shared z3"
  MSYS2_ARG_CONV_EXCL="-DCMAKE_INSTALL_PREFIX=" \
  ${MINGW_PREFIX}/bin/cmake.exe \
    -G"Ninja" \
    -DCMAKE_INSTALL_PREFIX=${MINGW_PREFIX} \
    -DZ3_BUILD_LIBZ3_SHARED=ON \
    -DZ3_BUILD_TEST_EXECUTABLES=OFF \
    -DZ3_INCLUDE_GIT_HASH=OFF \
    -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
    -DPython3_EXECUTABLE=${MINGW_PREFIX}/bin/python.exe \
    "${extra_config[@]}" \
    ../${_realname}-${_realname}-${pkgver}

  ${MINGW_PREFIX}/bin/cmake.exe --build ./
}

check() {
 cd "${srcdir}"/build-${MSYSTEM}-shared
 ${MINGW_PREFIX}/bin/ctest.exe test-z3 || true
}

package() {
  cd "${srcdir}"/build-${MSYSTEM}-static
  DESTDIR="${pkgdir}" ${MINGW_PREFIX}/bin/cmake.exe --install .

  cd "${srcdir}"/build-${MSYSTEM}-shared
  DESTDIR="${pkgdir}" ${MINGW_PREFIX}/bin/cmake.exe --install .

  if [[ ${CARCH} != i686 ]]; then
    MSYS2_ARG_CONV_EXCL="-p" python -m compileall \
      -o 0 -o 1 -q -s"${pkgdir}" -p"/" "${pkgdir}${MINGW_PREFIX}/lib/python"*
  fi

  install -Dm644 "${srcdir}"/${_realname}-${_realname}-${pkgver}/LICENSE.txt \
    "${pkgdir}"${MINGW_PREFIX}/share/licenses/${_realname}/LICENSE.txt
}
